Nuprl Lemma : pairwise-nil
11,40
postcript
pdf
P
:Top. (
x
,
y
[].
P
(
x
,
y
))
True
latex
Definitions
x
:
A
.
B
(
x
)
,
P
Q
,
(
x
,
y
L
.
P
(
x
;
y
))
,
True
,
P
&
Q
,
P
Q
,
P
Q
,
t
T
,
||
as
||
,
Y
,
{
i
..
j
}
,
i
j
<
k
,
A
B
,
A
,
False
,
Lemmas
int
seg
wf
,
true
wf
,
top
wf
origin
P:Top. (x,y
[]. P(x,y)) 
True P:Top. (x,y[]. P(x,y)) True x:A. B(x) Qx,yL. P(x;y)) Q Q T
}
j < k B
A